$\forall$$X$:Type, ${\it eq}$:EqDecider($X$), $f$, $g$:$x$:$X$ fp$\rightarrow$ Type. $g$ $\subseteq$ $f$ $\Rightarrow$ \{$\forall$$x$:$X$. $f$($x$)?Top $\subseteq\rho$ $g$($x$)?Top\}